enrich
   array_of_nat, 
   map_nat_nat, 
   partition, 
   list_of_nat, 
   set_of_nat
with
   
   
   functions  . [ . ] : mapnatnat × nat × nat × nat → mapnatnat prio 2 right;
              ⟦ . ⟧ : partelem → arrnat → natset;
              list2set : natlist → natset;
              resetcnt : partition → partition;
   predicates  DAid : arrnat × mapnatnat;
               ADid : arrnat × mapnatnat;
               nodups : arrnat;
               split : partition × arrnat × natlist;
               splitone : partelem × arrnat × natlist;
               . ∈ . : nat × partelem prio 5 right;
               okp : partelem × nat;
               partitions : partition × nat;
               divides : partition × partition × natlist × arrnat;
               XornoX : partelem × natlist × arrnat;
               startorfin : partelem × partition;
               Fok : mapnatnat × partition × nat;
               samepartitions : partition × arrnat × partition × arrnat;
               partitionRefinement : partition × arrnat × partition × arrnat × natlist;
   procedures MAIN natlist : arrnat, mapnatnat, partition, mapnatnat nonfunctional ;;
              REFINE natlist, mapnatnat : arrnat, mapnatnat, partition nonfunctional ;;
              REFINEONE nat, mapnatnat : arrnat, mapnatnat, partition nonfunctional ;;
              NEWPARTS  : partition, mapnatnat nonfunctional ;;
   variables  i : nat;
              x : nat;
              F : mapnatnat;
              Pdone : partition;
              Pnew : partition;
              length_of_P : nat;
              p1 : partelem;
              partelem-sem : arrnat → natset;

   

   axioms list2set-def :  ⊦ n ∈ list2set(X) ↔ n ∈ X;
          partitionRefinement-def
          : 
            ⊦   partitionRefinement(P, A, P0, A0, X)
              ↔ (∀ p. 
                     p ∈ P
                   → (∃ p0. p0 ∈ P0 ∧ (⟦p⟧ (A) = ⟦p0⟧ (A0) ∩ list2set(X) ∨ ⟦p⟧ (A) = ⟦p0⟧ (A0) \ list2set(X))));
          samepartitions-def
          :  ⊦ samepartitions(P, A, P0, A0) ↔ # P = # P0 ∧ (∀ n. n < # P → ⟦P[n]⟧ (A) = ⟦P0[n]⟧ (A0));
          partelem-sem-def :  ⊦ n ∈ ⟦p⟧ (A) ↔ (∃ m. m ∈ p ∧ A[m] = n);
          Fok-def :  ⊦ Fok(F, P, n0) ↔ (∀ n. n < n0 → n ∈ F ∧ F[n] < # P ∧ n ∈ P[F[n]]);
          nodups-def :  ⊦ nodups(A) ↔ (∀ m, m0. m ≠ m0 ∧ m < # A ∧ m0 < # A → A[m] ≠ A[m0]);
          resetcnt-empty :  ⊦ resetcnt([]) = [];
          resetcnt-rec :  ⊦ resetcnt(p ' + P) = p.count:= 0 + resetcnt(P);
          DAid-def :  ⊦ DAid(A, D) ↔ (∀ n. n < # A → A[n] ∈ D ∧ D[A[n]] = n);
          ADid-def :  ⊦ ADid(A, D) ↔ (∀ m. m ∈ D → D[m] < # A ∧ A[D[m]] = m);
          split-def :  ⊦ split(P, A, X) ↔ (∀ p. p ∈ P → okp(p, # A) ∧ splitone(p, A, X));
          splitone-def :  ⊦ splitone(p, A, X) ↔ (∀ n. n ∈ p → (n < p.first + p.count ↔ A[n] ∈ X));
          okp-def :  ⊦ okp(p, n) ↔ p.first ≤ p.last ∧ p.first + p.count ≤ p.last + 1 ∧ p.last < n;
          partititions-def
          : 
            ⊦   partitions(P, n0)
              ↔ (∀ n. 
                     n < n0 → (∃ m. m < # P ∧ n ∈ P[m] ∧ (∀ m0. m0 < # P ∧ m0 ≠ m → ¬ n ∈ P[m0])));
          inpartelem-def :  ⊦ n ∈ p ↔ p.first ≤ n ∧ n ≤ p.last;
          updF-member :  ⊦ m0 ∈ F[m, n, i] ↔ m0 ∈ F;
          updF-get :  ⊦ m0 ∈ F → F[m, n, i][m0] = (m ≤ m0 ∧ m0 ≤ n ⊃ i;F[m0]);
          divides-def :  ⊦ divides(P, P0, X, A) ↔ (∀ p. p ∈ P → XornoX(p, X, A) ∧ startorfin(p, P0));
          startorfin-def
          : 
            ⊦   startorfin(p, P0)
              ↔ (∃ p0. p0 ∈ P0 ∧ (p0.first = p.first ∧ p.last ≤ p0.last ∨ p0.first ≤ p.first ∧ p0.last = p.last));
          XornoX-def :  ⊦ XornoX(p, X, A) ↔ (∀ n. n ∈ p → A[n] ∈ X) ∨ (∀ n. n ∈ p → ¬ A[n] ∈ X)

   

   declarations MAIN : MAIN(X; A, D, P, F){REFINE(X, F; A, D, P); NEWPARTS(; P, F)};
                REFINE : REFINE(X, F; A, D, P){while X ≠ [] do {REFINEONE(X.head, F; A, D, P); X := X.tail}};
                REFINEONE
                : REFINEONE(x, F; A, D, P)
                  {if x ∈ D
                   then let i = D[x]
                        in let p = P[F[i]]
                           in if i < p.first + p.count
                              then skip
                              else {if i ≠ p.first + p.count
                                    then {A := A[i, A[p.first + p.count]][p.first + p.count, A[i]]; D := D[A[i], i]; 
                                          D := D[A[p.first + p.count], p.first + p.count]}; 
                                    P := P[F[i], p.count:= (p.count + 1)]}
                  }
                ;comment: optimized to avoid empty swap when i = p.first + p.count;
                NEWPARTS
                : NEWPARTS(; P, F)
                  {let Pdone = [], Pnew = [], length_of_P = # P
                   in {while P ≠ []
                       do let p = P.head
                          in {P := P.tail; 
                              if p.count ≠ 0 ∧ p.first + p.count ≤ p.last
                              then Pdone := Pdone + pe(p.first, p.first + p.count -1, 0), Pnew := Pnew + pe(p.first + p.count, p.last, 0), 
                                   F := F[p.first + p.count, p.last, length_of_P + # Pnew]
                              else Pdone := Pdone + p}; 
                       P := Pdone + Pnew}
                  }
                ;comment: spec is buggy. Second first slot must be p.first + p.count not p.count;
end enrich